\section{Módulo Diccionario Trie($\alpha$)}

\begin{Interfaz}
  
	\textbf{parámetros formales}\hangindent=2\parindent\\
	\parbox{1.7cm}{\textbf{géneros}} $\alpha$

	\textbf{se explica con}: \tadNombre{Diccionario(String, $\alpha$)}

	\textbf{géneros}: \TipoVariable{dicctrie($\alpha$)}.
	
	\Titulo{operaciones}

	\InterfazFuncion{Vacío}{}{dicctrie($\alpha$)}%
	{$\somb{res} \igobs $ vacío}
	[$\Theta(1)$]
	[Genera un diccionario vacío.]

	\InterfazFuncion{Definir}{\Inout{d}{dicctrie($\alpha$)}, \In{clave}{string}, \In{significado}{$\alpha$}}{}
	[$\somb{d} \igobs d_0$]
	{$\somb{d} \igobs \textrm{definir}(\somb{clave}, \somb{significado}, d_0)$ $\land$ alias(obtener($\somb{clave}, \somb{d}$) $\igobs$ $\somb{significado}$)}
	[$\Theta(|clave|)$]
	[Define en el diccionario la clave $clave$ con el valor $significado$.]
	
	\InterfazFuncion{Definido?}{\In{d}{dicctrie($\alpha$)}, \In{clave}{string}}{bool}
	{$\somb{res} \igobs \textrm{def?}(\somb{clave}, \somb{d})$}
	[$\Theta(|clave|)$]
	[Verifica que la clave $clave$ este definida en el diccionario $d$.]
	
	\InterfazFuncion{Obtener}{\In{d}{dicctrie($\alpha$)}, \In{clave}{string}}{$\alpha$}
	[$\textrm{def?}(\somb{clave}, \somb{d})$]
	{$\somb{res} \igobs \textrm{obtener}(\somb{clave}, \somb{d})$ $\land$ alias($\somb{res}$ $\igobs$ obtener($\somb{clave}, \somb{d}$))}
	[$\Theta(|clave|)$]
	[Devuelve el significado de la clave $clave$ en el diccionario $d$.]
  
  
\end{Interfaz}

\begin{Representacion}
	\Titulo{Representación de dicctrie}

	\begin{Estructura}{dicctrie($\alpha$)}[puntero(nodo)]
		\begin{Tupla}[nodo]
			\tupItem{definido}{bool}%
			\tupItem{dato}{$\alpha$}%
			\tupItem{siguientes}{arreglo[256] de puntero(nodo)}%
		\end{Tupla}
	\end{Estructura}

	
	\Rep[$\somb{puntero(nodo)}$][e]{($e$ $=$ NULL) \oluego (NoTieneCiclos($e$) \yluego TerminaDefinido($e$))}
	
	~
	\tadOperacion{NoTieneCiclos}{puntero(nodo)/p}{bool}{$\neg$(p = NULL)}
	\tadAxioma{NoTieneCiclos($p$)}{NoTieneCiclosAux($p \puntito <>$,$<>$)}

	~
	\tadOperacion{NoTieneCiclosAux}{secu(puntero(nodo)),secu(puntero(nodo))}{bool}{}
	\tadAxioma{NoTieneCiclosAux($avisitar$,$visitados$)}{
		vacía?($avisitar$) \oluego $\neg$(está?(prim($avisitar$),$visitados$)) \yluego
		NoTieneCiclosAux( Siguientes(prim($avisitar$)) \& fin($avisitar$), prim($avisitar$) \puntito $visitados$ )
	}

	~
	\tadOperacion{Siguientes}{puntero(nodo)/p}{secu(puntero(nodo))}{$\neg$(p = NULL)}{}
	\tadAxioma{Siguientes($p$)}{SiguientesAux($p$\DRef siguientes, 256)}

	~
	\tadOperacion{SiguientesAux}{ad(puntero(nodo))/arr,nat/n}{secu(puntero(nodo))}{(\paratodo{nat}{i}) ($i < 256$) $\implies$ definido?($arr$,$i$)}
	\tadAxioma{SiguientesAux($arr$,$n$)}{
		\IF $n = 0$
			THEN $\secuencia{}$
			ELSE
			{
				\IF $arr[n-1] = NULL$
					THEN SiguientesAux($arr$,$n-1$)
					ELSE $arr[n-1]$ $\puntito$ SiguientesAux($arr$,$n-1$)
				FI
			}
		FI
	}
	
	~
	\tadOperacion{TerminaDefinido}{puntero(nodo)/p}{bool}{$\neg$(p = NULL)}
	\tadAxioma{TerminaDefinido($p$)}{
		\IF vacía?(siguientes($p$)) THEN $p$\DRef definido ELSE TerminaDefinidoAux(siguientes($p$)) FI
	}

	~
	\tadOperacion{TerminaDefinidoAux}{secu(puntero(nodo))/s}{bool}{(\paratodo{puntero(nodo)}{p})(esta?($p$, $s$) $\impluego$ $\neg$($p$ $=$ NULL))}
	\tadAxioma{TerminaDefinidoAux($s$)}{
		vacía?($s$) \oluego TerminaDefinido(prim($s$)) $\land$ TerminaDefinidoAux(fin($s$)))
	}

	~
	
	\Abs[puntero(nodo)]{dicc(string, $\alpha$)}[e]{d}{
		(\paratodo{string}{s})((def?(s, d) \ssi ExisteRama($s$, $e$)) \yluego (def?($s$, $d$) \impluego (obtener($s$, $d$) \igobs ObtenerValor($s$, $e$))))
	}
	
	~
	
	\tadOperacion{ExisteRama}{string, puntero(nodo)}{bool}{}
	\tadAxioma{ExisteRama($s$, $p$)}{
		vacía?($s$) \oluego ($\neg$($p$ $=$ NULL) \yluego (definido?(ord(prim($s$)), $p$\DRef siguientes) \yluego ExisteRama(fin($s$), $p$\DRef siguientes[ord(prim($s$))])))
	}
	
	\vspace{10pt}
	~
	
	\tadOperacion{ObtenerValor}{string/s, puntero(nodo)/p}{$\alpha$}{ExisteRama($s$, $p$)}
	\tadAxioma{ObtenerValor($s$, $p$)}{
		\IF vacía?($s$) THEN $p$\DRef dato ELSE ObtenerValor(fin($s$), $p$\DRef siguientes[ord(prim($s$))])) FI
	}
	
	~
\end{Representacion}

\begin{Algoritmos}

\Implementacion{iVacío}{}{puntero(nodo)}
\begin{algorithmic}
	\State \res \asignar NULL
\end{algorithmic}

~

\Implementacion{iDefinir}{\Inout{d}{puntero(nodo)}, \In{clave}{string}, \In{significado}{$\alpha$}}{}
\begin{algorithmic}
	\State var i, len : nat
	\State var p, padre : puntero(nodo)
	\If{d = NULL}
		\State d \asignar crearNodo()
	\EndIf
	\State p \asignar d
	\State padre \asignar d
	\State len \asignar Longitud(clave)
	\State i \asignar 0
	\While{i $<$ len}
		\State p \asignar (*padre).siguientes[ ord(clave[i]) ]
		\If{p = NULL}
			\State p \asignar crearNodo()
			\State (*padre).siguientes[ ord(clave[i]) ] \asignar p
		\EndIf
		\State padre \asignar p
		\State i \asignar i + 1
	\EndWhile
	\State (*p).definido \asignar true
	\State (*p).dato \asignar significado
\end{algorithmic}

~

\Implementacion{iDefinido?}{\In{d}{puntero(nodo)}, \In{clave}{string}}{bool}
\begin{algorithmic}
	\State var p : puntero(nodo) \asignar obtenerNodo( d, clave )
	\State \res \asignar $\neg$(p = NULL) \yluego (*p).definido
\end{algorithmic}

~

\Implementacion{iObtener}{\In{d}{puntero(nodo)}, \In{clave}{string}}{bool}
\begin{algorithmic}
	\State var p : puntero(nodo) \asignar obtenerNodo( d, clave )
	\State \res \asignar (*p).dato
\end{algorithmic}

~

\Implementacion{crearNodo}{}{puntero(nodo)}
\begin{algorithmic}
	\State var n : nodo
	\State var i : nat
	\State n.definido \asignar false
	\State i \asignar 0
	\While{i $< 256$}
		\State n.siguientes[i] \asignar NULL
		\State i \asignar i + 1
	\EndWhile
	\State \res \asignar \&n
\end{algorithmic}

~

\Implementacion{obtenerNodo}{\In{d}{puntero(nodo)}, \In{clave}{string}}{puntero(nodo)}
\begin{algorithmic}
	\State var i : nat \asignar 0
	\State var len : nat \asignar Longitud(clave)
	\State var p : puntero(nodo) \asignar d
	\While{i $<$ len}
		\If{p = NULL}
			\State i \asignar len
		\Else
			\State p \asignar (*p).siguientes[ ord(clave[i]) ]
			\State i \asignar i + 1
		\EndIf
	\EndWhile
	\State \res \asignar p
\end{algorithmic}

\end{Algoritmos}
